COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00006 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂AIL {skip 4}Professor Charles Akemann↓Department of Mathematics
↓U. C. Santa Barbara↓Santa Barbara, CA 93106∞

Dear Professor Akemann:

	I feel flattered to be asked to write a recommendation
for Martin Davis.  I won't write about his world-wide reputation
in mathematical logic and recursive function theory 
because
he has undoubtedly as references, people who also have
substantial reputation in that field.  
(For me to
write about his role in settling Hilbert's tenth problem could only
serve to show that I am not a complete illiterate in the area,
but can't add anything to his fame.)
I can, however, write
about his work connected with computation and artifical intelligence.

	Martin Davis was one of the first people, and perhaps even
the very first person, to write a computer program for proving
sentences in first order logic, and he was one of the first to
encounter the difficulties that interfere with making a computer program
which can match human performance in first order theorem proving.
While he didn't make it his main field of activity, he retuurns
to it from time to time, always with a substantial contribution.

	Recently, partly in collaboration with Jack Schwartz, he
has begun studying the problem of proving programs correct.  Their
approach seems promising, but since Martin has just returned to
NYU and Jack is on sabbatical, it probably hasn't advanced far into
actual implementation.  Should he move that work to Santa Barbara,
I believe it will greatly benefit both computer science and mathematics.

	Last year Martin spent a month at the Stanford Artificial
Intelligence Laboratory which he followed with biweekly visits.  His expertness
in mathematical logic was of great assistance to our theorem proving
and proof checking work.  Besides that, he helped clarify the
mathematical nature of a proposed method for making computer programs
"jump to conclusions" from insufficient data, something we have
become convinced is necessary if artificial intelligence is to be
achieved.  Martin is a delightful collaborator, and our graduate
students gained much from his presence, short as it was.
Of all the famous mathematical logicians, he and Dana Scott have
been the most helpful to computer science.

	The prospect of having him on the West Coast again
is very attractive.

.sgn